Definitions | t T, ma-valtype(da; k), Kind-deq, Knd, x:A. B(x), (x l), b, prop{i:l}, A,  b, , deq-member(eq; x; L), P  Q, P Q, P   Q, Unit, event-info(ds;da), decl-state(ds), top, fpf-cap(f; eq; x; z), if b then t else f fi ,  x,y. t(x;y), list_accum(x,a.f(x;a); y; l), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ecl-trans-state-from(v; z; L), ecl-trans-type(A), ecl-trans-tuple{i:l}(ds; da), Id,  x. t(x), fpf(A; a.B(a)) |